D:Dsys.
(i:Id. AtomFree(da(M(i))))
 (i:Id. AtomFree(Type;{m:(l:IdLnkt:IdM(source(l)).dout(l,t))| source(mlnk(m)) = i })) 

latex

Definitions	Dsys, t  T, x:A. B(x), da(M), KindDeq, Knd, AtomFree(d), x:AB(x), Prop, P  Q, source(l), M(i), M.dout(l,tg), Id, x:AB(x), IdLnk, Type, AtomFree(T;x), x.A(x), f(a), s ~ t, Void, s = t, mlnk(m), x. t(x), #$n, a<b, False, A, AB, , {x:A| B(x) }, , Atom, A/x,y. B(x;y), 1of(t)
Lemmas	atom-free-settype, atom-free-ma-dout, lsrc wf, IdLnk wf, atom-free-IdLnk, atom-free-Id, ma-dout wf, Id wf, atom-free-decl wf, Knd wf, Kind-deq wf, ma da wf, d-m wf, dsys wf